Nuprl Lemma : filter-concat
11,40
postcript
pdf
T
:Type,
P
:(
T
),
L
:(
T
List List). filter(
P
;concat(
L
)) ~ concat(map(
l
.filter(
P
;
l
);
L
))
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
filter(
P
;
l
)
,
concat(
ll
)
,
map(
f
;
as
)
,
reduce(
f
;
k
;
as
)
,
Y
,
Top
,
S
T
Lemmas
bool
wf
,
concat-cons
,
top
wf
,
filter
append
sq
origin
T:Type, P:(T
), L:(T List List). filter(P;concat(L)) ~ concat(map(
l.filter(P;l);L)) T:Type, P:(T), L:(T List List). filter(P;concat(L)) ~ concat(map(l.filter(P;l);L)) x:A. B(x)
T
T